es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E. (f2f+-p+(e,e'))  (e < e') 

latex

Definitions	x:A. B(x), P  Q, t  T, R1 => R2, x f y, Trans(T;x,y.E(x;y)), P & Q, A c B, , f2f+-p+
Lemmas	f2f+-property, f2f+-p+ wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, rel plus minimal, f2f+-pred wf, es-causl wf, f2f+-pred-sub-causl, es-causl transitivity2, es-causle weakening